class Test {
    static void main() {
		int x <= 5-4*2;
		// ERROR, x is int
		x <= 2L + 2;

		// Length error
		x <= x.length;

		// redefine variable
		long x;
    }		
}

class Child extends Parent{
	int f;
	
	
    int f3(int a) {
        		pre:a>0;
		post: a>0;
		
		while (a>0){
			int t;
			t <= 3;
		}

		
		int t <= 3;

		
		a <= this.f2(true);

       	return a;
	}
	
	// function has the same name with field
	 int f(long a){

		
		pre:a > 1;


		post: i>0;
		int i <= 42;
		return 0;
	}
	
	// another functon
	 int f2(boolean b){
		pre:b>0;
		post: b;

		
		return b;
	}
}

// cyclic inheritance
class Parent extends Child{
	int p;
}

// inherits not existed class
class someclass extends class_not_exist{
}